Wir entwickeln den parallelen Hochleistungsbeweiser P A R E D U X, der auf der Methode der Termersetzungssysteme beruht, durch Parallelisieren unseres Beweisers R E D U X auf den Systemumgebungen VS-T HREADS und DTS. PaReDuX enthält verschiedene Beweismethoden wie induktive Vervollständigung, Knuth-Bendix Vervollständigung, AC-Vervollständigung und unfailing completion Ausgehend von ReDuX werden diese Methoden in Theorie und Praxis so parallelisiert, daß sie auf unseren Multiprozessor Arbeitsplatzrechnern signifikant schneller werden. Im Berichtszeitraum wurden die Fälle der Basisvervollständigung, der AC-Vervollständigung und der unfailing completion auf shared memory Multiprozessoren behandelt und in mehreren Arbeiten veröffentlicht. Als Anwendungen dienten hauptsächlich Probleme der Gruppentheorie.
Dieses Projekt wird seit Mitte 1993 von der DFG Rahmen des Schwerpunktprogramms ,,Deduktion`` gefördert.
Dr. Beatrice Amrhein